M.sends(k,s,v)
== concat(map(pL.tagged-messages((pL.1).2;s;v;pL.2)
== concat(map;fpf-vals(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);p.eqof(KindDeq)
== concat(map;fpf-vals(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);p.((p.1)
== concat(map;fpf-vals(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);p.,k);(M.2.2.2.2.2).1))) 

latex

Definitions	M.sends(k,s,v), concat(ll), map(f;as), tagged-messages(l;s;v;L), fpf-vals(eq;P;f), product-deq(A;B;a;b), Knd, IdLnk, IdLnkDeq, eqof(d), KindDeq, t.1, t.2
FDL editor aliases	ma-send-val